es:ES, i:Id, L:IdLnk List, T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 (e1, e2:E.
 ((lL.kind(e1) = rcv(lnk-inv(l),"encrypt")  Knd)
 ( (lL.kind(e2) = rcv(lnk-inv(l),"encrypt")  Knd)
 ( 2of(val(e1)) = 2of(val(e2))  Atom1
 ( e1 = e2) 

latex

Definitions

"$x", Prop, P  Q, Id, x. t(x), t  T, x:A. B(x), b, next(tab), Top, P  Q, if b t else f fi, outl(x), true, false, 2of(t), P & Q, isl(x), P  Q, T, True, 1of(t), encrypt(tab;keyv), let x,y,z = a in t(x;y;z), ptr(tab), {T}, SQType(T), rcv(l,tg), isrcv(k), es-secret-server, (xL.P(x)), xL. P(x), state dsk:A sends [tg, e.f(e):B] on l, x:A. B(x), A & B, @i events of kind k change x to f State(ds) (val:T), e@i. P(e), let x = a in b(x), x(s), , False, , Unit, {i..j}, P  Q, e  e' , secret-table(T), lnk(k), , x when e

Lemmas

Knd wf, es-secret-server wf, es-E wf, nat wf, l exists wf, es-kind wf, es-val wf, lnk-inv wf, Id wf, event system wf, IdLnk wf, rcv wf, pi2 wf, st-length wf, false wf, assert of lt int, le wf, lsrc-inv, iff transitivity, es-kind-rcv, es-when wf, fpf-cap-single, lsrc wf, st-atom wf, assert of le int, eqof eq btrue, ldst wf, true wf, es-loc-rcv, bnot wf, assert wf, eqtt to assert, bool wf, bnot of lt int, le int wf, id-deq wf, es-sender wf, squash wf, st-ptr wf, eqff to assert, lt int wf, es-vartype wf, es-loc-init, es-init wf, es-first-init, unit wf, int seg wf, st-next wf, ss-atoms-distinct, st-ptr-wf2, isl wf, fpf-cap-single1, es-le-total, ss-ptr-non-decreasing, secret-table wf, data wf, IdLnk sq, Knd sq, lnk wf, isrcv wf